/**                   GNU GENERAL PUBLIC LICENSE
 *                       Version 3, 29 June 2007
 *
 * Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
 * Everyone is permitted to copy and distribute verbatim copies
 * of this license document, but changing it is not allowed.
 * See License.txt file that comes with this distribution
 *
 *
 * Author: Vitaly German <vitaly.german@gmail.com>, (C) 2007-2008
 * 
 **/

#pragma once
#include <boost/bind.hpp>
#include "math_builder2.hpp"

template <class Node, class KeyT = MarkT>
struct LogicB {
    typedef Key2Fun< typename boost::function<void (Node)> , KeyT, MarkTrait > type;
};

template <class Node, class B>
class LogicBuilder {
    SolverEnv_aptr env;
    B build;

public:
    LogicBuilder(SolverEnv_aptr env1):env(env1){
    	init(build);
    }
    void operator()(Node & n){
	build(n);
    }
private:
    void init(B&);

    void make_and(Node);
    void make_or(Node);
    void make_not(Node);
    void make_forall(Node);
    void make_exists(Node);
    
    void make_lterm(Node);

    void make_default(Node);
    /// helper methods
    ///F_Declaration_aptr cannot be const 
    void declare_vars(const F_Declaration_aptr& quantifier, Node vars);
};

template <class Node, class B>
void LogicBuilder<Node,B>::make_and(Node node){
    rfm_solver::debug("\n===make_and");
    F_And_aptr  f_and1(env->get_root()->add_and());
    env->set_root(f_and1);
    build(node.children[0]) ;
    env->set_root(f_and1);
    build(node.children[1]) ;
}

template <class Node, class B>
void LogicBuilder<Node,B>::make_or(Node node){
    rfm_solver::debug("\n===make_or");
    F_Or_aptr  f1(env->get_root()->add_or());
    env->set_root(f1);
    build(node.children[0]) ;
    env->set_root(f1);
    build(node.children[1]) ;
}

template <class Node, class B>
void LogicBuilder<Node,B>::make_not(Node node){
    rfm_solver::debug("\n===make_not");
    F_Not_aptr f1(env->get_root()->add_not());
    env->set_root(f1);
    build(node.children[0]);
}


class VaribleDeclarer {
    SolverEnv_aptr env;
    F_Declaration_aptr decl;

public:
    VaribleDeclarer(SolverEnv_aptr & env1, F_Declaration_aptr decl1):env(env1),decl(decl1) {};

    template <class Node>
    void operator()( const Node & node ){
	assert(node.value.id() == calculator::variableID);
        std::string svar(node.value.begin(), node.value.end());
	Variable_ID var  = decl->declare(svar);
        rfm_solver::debug("+++Variable ",var, " declared.");
        env->update_variable(var, svar);
    }
};

template <class Node, class B>
void LogicBuilder<Node,B>::make_forall(Node node) {
    rfm_solver::debug("\n===make_forall");
    assert(node.value.id() == calculator::quantifierID);

    F_Forall_aptr qf(env->get_root()->add_forall());

    rfm_solver::debug("+++Forall created.");
    declare_vars(qf, node.children[0]);
    env->set_root(qf);
}

template <class Node, class B>
void LogicBuilder<Node,B>::make_exists(Node node){
    rfm_solver::debug("\n===make_exists");
    assert(node.value.id() == calculator::quantifierID);

    F_Exists_aptr qf(env->get_root()->add_exists());

    rfm_solver::debug("+++Exists created.");
    declare_vars(qf, node.children[0]);
    env->set_root(qf);
}

template <class Node, class B>
void LogicBuilder<Node,B>::declare_vars(const F_Declaration_aptr&quantifier, Node vars) {
    VaribleDeclarer vd(env, quantifier);
    if (vars.value.id() == calculator::variableID) {
        vd(vars);
    } else if (vars.value.id() == calculator::var_listID) {
        std::for_each(
            vars.children.begin(),
            vars.children.end(),
            boost::bind<void>(boost::ref(vd), _1)
        );
    } else
        assert(1 && "Unknown node");
}

template <class Node, class B>
void LogicBuilder<Node,B>::make_lterm(Node node){
     rfm_solver::debug("\n===make_lterm");
     rfm_solver::debug("\nart: ",node.children.size());
     assert(node.children.size()==1 || node.children.size()==2);
     std::for_each(
	node.children.begin(),
	node.children.end(),
     	boost::bind<void>(boost::ref(build), _1)
     );
}

template <class Node, class B>
void LogicBuilder<Node,B>::make_default(Node node){
    rfm_solver::debug("\n===make_default. Val id: ");
     build.stat();
    /// call 
    assert(node.value.id() == calculator::equsID && "Inequality expected.");

    typedef typename LogicB <Node>::type CB2F;

    CB2F k2f;
    ConstraintBuilder2<Node, CB2F> cb(env, k2f);
    RegConstraintBuilder2Fun(cb, k2f);
    
    F_And_aptr new_root = cb(node);
    env->set_root(new_root);
}

template <class Node, class B>
void LogicBuilder<Node,B>::init(B& b){
     rfm_solver::debug("\n===init");
    typedef LogicBuilder<Node,B> LB;
    //LB & lb = *this;
    
    MarkManagerT & mrk = MarkManagerT::instance();
    
    b.RegisterFun(mrk.andl, boost::bind(&LB::make_and, this, _1));
    b.RegisterFun(mrk.orl, boost::bind(&LB::make_or, this, _1));
    b.RegisterFun(mrk.notl, boost::bind(&LB::make_not, this, _1));
    b.RegisterFun(mrk.forall, boost::bind(&LB::make_forall, this, _1));
    b.RegisterFun(mrk.exists, boost::bind(&LB::make_exists, this, _1));
    
    b.RegisterFun(mrk.lterm, boost::bind(&LB::make_lterm, this, _1));
    
    b.RegisterFun(mrk.null, boost::bind(&LB::make_default, this, _1 ), true ); //default
}



struct BuildFMERProblem
{
    template <class Node>
    Relation_aptr operator () (Node &node) const {
	
#ifdef DEBUG
        debug("\n===Input node===:\n");
	prn(node);
        debug("\n===Input node===:\n");
#endif
        /// Constrct/Init
        Relation_aptr rel = Relation::make();
        rfm_solver::debug("+++Relation created.");
        
        SolverEnv_aptr env_aptr(new SolverEnv(rel));
        typedef typename LogicB<Node>::type Lb_k2f;
        LogicBuilder<Node, Lb_k2f> logic_builder(env_aptr);

        /// Real processin
        logic_builder(node);
#ifdef DEBUG
        debug("\n===Builded relation:===\n");
	rel->print();
	debug(""); //make flush
#endif
        return rel;
    }
};
